g:GrpSig, a, b:|g|. SqStable(a  b) 

latex

Up	groups 1
Definitions of Statement	a  b
Definitions	t  T, x f y, a  b, x:A. B(x), P  Q
Lemmas	grp sig wf, grp car wf, decidable assert, grp le wf, assert wf, sq stable from decidable